\documentclass[10pt,a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{graphicx}
\usepackage{enumerate}

\newcommand{\dist}[2]{d_{#1#2}}
\newcommand{\distij}{\dist{i}{j}}
\newcommand{\distji}{\dist{j}{i}}
\newcommand{\distik}{\dist{i}{k}}
\newcommand{\pij}{p_{ij}}
\newcommand{\eqg}{G_{\sigma}^{=}}
\newcommand{\aqg}{A_{\sigma}^{=}}
%\newcommand{\eqtback}[1]{\overset{\twoheadleftarrow}{\rule{0pt}{1.2ex}\smash{\eqt}}(#1)}
%\newcommand{\eqtforw}[1]{\overset{\twoheadrightarrow}{\rule{0pt}{1.2ex}\smash{\eqt}}(#1)}
\newcommand{\eqtback}[2][]{\overset{\twoheadleftarrow}{\rule{0pt}{1.2ex}\smash{\eqt_{#1}}}(#2)}
\newcommand{\eqtforw}[2][]{\overset{\twoheadrightarrow}{\rule{0pt}{1.2ex}\smash{\eqt_{#1}}}(#2)}
\newcommand{\eqt}{\eqts{\sigma}}
\newcommand{\eqtw}{\widetilde{\eqtree}^{\sigma}}
\newcommand{\eqts}[1]{\eqtree^{#1}}
\newcommand{\eqtree}{\mathcal{T}}
\newcommand{\act}{\mathcal{O}}
\newcommand{\sg}{\widetilde{G}}
\newcommand{\sact}{\widetilde{\act}}
\newcommand{\sa}{\widetilde{A}}
\newcommand{\s}{\mathcal{S}^\sigma}
\newcommand{\f}{\mathcal{F}^\sigma}
%\newtheorem{theorem}{Theorem}
\newtheorem{definition}{Definition}
\newtheorem{lemma}{Lemma}
\newtheorem{notation}{Notation}
%\newproof{proof}{Proof}
\newtheorem{assumption}{Assumption}
\DeclareMathOperator*{\argmin}{arg\,min}

\begin{document}
Začnu definicí zkratek abych ušetřil písmena v dalším textu.
\begin{notation}
E = Early\\
SE = Strictly early\\
L = Late\\
SL = Strictly late\\
AET = Active equality tree\\
\end{notation}

Omlouvám se za trochu nekonzistentní značení u obou obrázků, ale myslím, že i tak by to mělo být snadno pochopitelné.

Uvažuji jeden krok push nějakého AET (na obrázku je to $\eqt$) ve kterém mi odpadne kousek stromu (na obrázku je to $A$ - budu ho nazývat "odpadlík") a ptám se, zda tenhle odpadlý kousek stromu je on-time AET. 

Jestli po odpadnutí odpadlíka i to co mi zbylo k dalšímu shiftování (na obrázku je to $B$) je AET zatím nijak neuvažuji. To už vím že není, protože když se posunu někam extrémně doprava, pak se může každý uzel stát SL, takže ani jediná hrana v tom posunovaném stromu nebude moct být active. Ale jak se ukáže v následujícím textu, tak ten strom který posouvám vůbec (během posouvání) AET být nemusí (jen na startu to musí být on-time AET), přesto všichni odpadlíci budou on-time AET.

Poznámka: v následujícím textu budu mluvit např o hraně $[i,j]$. Zápis volím takto, aby bylo zřejmé, že orientace může být $i\rightarrow j$ nebo $i\leftarrow j$ - vždy to bude v textu jasně určeno.

\begin{figure}
	\centering
	\includegraphics[scale=0.5]{activate-fig}
\end{figure}

\begin{description}
\item[Algoritmus]:\\
\\Nechť algoritmus pro detekci odpadlíka funguje následovně (je to naprosto shodné s procedurou findNearestSplitEvent()). Uvažujeme teď v rozvrhu jen jediný strom, aby nás nerušily nárazy do jiných stromů. Tento předpoklad je zatím velmi důležitý a v druhé části textu budou úvahy rozšířeny i o nárazy do ostatních stromů v rozvrhu.

\begin{enumerate}[A)]
	\item Vezměme posunovaný strom a pivota určeme za kořen (viz obrázek). Pak dostaneme strom jehož hrany některé směřují směrem k pivotovi a některé od něj.
	
	\item Procházíme strom od listů a zkoumáme všechny hrany (průchod se nezastaví při prvním nalezeném odpadlíkovi, ale projde opravdu všechny hrany). Nechť $[i,j]$ je právě zkoumaná hrana (viz obrázek). 
	
	\item Pokud platí následující tři body zároveň, našli jsme odpadlíka.
	\begin{enumerate}
		\item \label{alg:podm1}($[i,j]$ směřuje k pivotovi AND děláme forward shift) NEBO ($[i,j]$ směřuje od pivota AND děláme backward shift)\footnote{Strom se mi nemůže rozpadnout na libovolné hraně - jen na takových hranách které "visí" na shiftovaném stromě. Ty hrany, do kterých shiftovaný strom "tlačí" nám odpadnout nemohou}
		\item \label{alg:podm2} Zajímá nás bod, ve kterém, podstrom $A$ (viz obrázek), který tato hrana odděluje přestává být SE v případě forward shiftu (resp. SL v případě backward shiftu)
		\item Pokud je tento bod blíže od startu shiftu, než poslední nalezený odpadlík, zapamatujeme si ho.
	\end{enumerate}
\end{enumerate}
Po dokončení algoritmu nemáme buď v ruce nic, nebo máme hranu a čas, na které nám vzniká nejbližší odpadlík.
\end{description}

\begin{description}
\item[Tvrzení k algoritmu]:\\
Začnu dvěma lemmaty, která mi později pomohou dokázat další tvrzení.

\begin{lemma}\label{lemma:zachovani}
Uvažujme libovolný graf $G$

Nechť $G$ je SE, pak po libovolném forward shiftu bude $G$ buď SE, E, on-time, L nebo SL. 

Nechť $G$ není SE (je jen E) nebo on-time, pak po libovolném forward shiftu bude $G$ E, on-time, L nebo SL.

Nechť $G$ není SL (je jen L) nebo on-time, pak po libovolném forward shiftu bude $G$ on-time, L nebo SL.

Nechť $G$ je SL, pak po libovolném forward shiftu bude $G$ vždy jen SL.

Analogicky pro backward shift.
\end{lemma}
\begin{proof}
Důkaz plyne z konvexnosti nákladové funkce $G$.
\end{proof}

Největším úskalím našich důkazů jsou ty lomené funkce. Jejich problém je v tom, že že hrana může být aktivní i když jedna její strana není "strictly" (např SE$\rightarrow$L, nebo E$\rightarrow$SL). Např pokud bychom uvažovali jen kvadratické funkce, toto by nikdy nenastalo, protože hrany by byly aktivní jen v případě SE$\rightarrow$SL (šmárjá to by se to  dokazovalo levou zadní a nemusel bych na tom trávit víkend). V důkazu korektnosti algoritmu, který přijde později, se budeme mimo jiné zabývat vlastnostmi stromu, který nám zůstane po odpadnutí odpadlíka. Pro tyto účely dokážeme nejprve několik lemmat, která nám zaručí, že pro všechny hrany $(i,j)$ v posouvaném stromu platí, že $\eqtforw{(i,j)}$ je SL. Jedinou výjimkou je startovní pozice, kdy se stromem ješt nebylo hnuto - tento stav bude v důkazu korektnosti algoritmu osvětlen sólo.

\begin{lemma}\label{lemma:forwardshift}
	Uvažujme on-time AET $\eqt$ a v něm hranu $(i,j)$ takovou že, $\eqtforw{(i,j)}$ není SL (je jenom L). Uvažujme shift $\eqt$ o lib $\delta>0$ (tj. forward shift). Pak platí, že $\eqtforw{(i,j)}$ po shiftu je SL. Analogicky pro hranu mezi E$\rightarrow$SL při backward shiftu.
\end{lemma}
\begin{proof}
	Hrana byla v $\eqt$ aktivní a $\eqtforw{(i,j)}$ nebylo SL tudíž $\eqtback{(i,j)}$ musel být před posunem SE. Pokud by $\eqtforw{(i,j)}$ nebyl po shiftu SL, znamenalo by to, že by se celý strom $\eqt$ vyplatilo posunout forward, což je spor, protože $\eqt$ byl on-time. ($\eqt$ byl před posunem zaseklý v pravém rohu plateu té společné nákladové funkce. Pro analogický případ v opačném směru je to uvízlé v levém rohu toho plateau. Pokud se pohybuje $\eqt$ někde mezi těmito dvěma body, je ta hrana SE$\rightarrow$SL.)
\end{proof}

Předchozí lemma nám říká, že jakmile je strom shiftnutý forward, tak pro všechny hrany $(i,j)$ z tohoto stromu platí, že $\eqtforw{(i,j)}$ je SL. 

Následující triviální lemma se nám bude velmi hodit.

\begin{lemma}\label{lemma:odtrzeninotSL}
	Nechť $G$ je libovolný SL graf. Uvažujme libovolný neprázdný vlastní podgraf $\widetilde{G}\subseteq G$ takový, že $\widetilde{G}$ není SL. Pak platí, že $G - \widetilde{G}$ je SL.
\end{lemma}
\begin{proof}
	Sporem: Nechť $G - \widetilde{G}$ není SL (je tedy z definice E), pak je zřejmé, že $((G-\widetilde{G})\cup \widetilde{G})$ je také E. Tudíž $G$ je E, což je spor s předpokladem, že $G$ je SL.
\end{proof}

Nyní ukážeme, že pokud bylo stromem již hnuto forward, tak i po odtržení nějakého odpadlíka bude stále pro libovolnou hranu ve zbývajícím stromu $(i,j)$ platit, že $\eqtforw{(i,j)}$ je SL:

\begin{figure}
	\centering
	\caption{Equality tree s odpadlíkem}\label{fig:odpadlik2-dk}
	\includegraphics[scale=0.7]{lemma-dk}
\end{figure}

\begin{lemma}\label{lemma:odpadlik2}
	Nechť $\eqt$ je equality tree takový, že každou jeho hranu $(i,j)\in A_{\eqt}$ platí, že $\eqtforw{(i,j)}$ je SL. Nechť algoritmus označí hranu $(k,l)\in A_{\eqt}$ pro rozpad ($\eqtback{(k,l)}$ zde představuje odpadlíka). Označme $\eqt_{*}=\eqtforw{(k,l)}$. Pak pro libovolnou hranu $(i,j)\in A_{\eqt_{*}}$ platí, že $\eqtforw[*]{(i,j)}$ je SL ($\eqtforw[*]{(i,j)}$ označuje pravý podstrom visící na této hraně ale jen v rámci $\eqt_{*}$). Analogicky pro backward shift.
\end{lemma}
\begin{proof}
	Uvažujme libovolnou hranu $(i,j)\in A_{\eqt_{*}}$. Mohou nastat dva případy:
	\begin{enumerate}[A)]
		\item\label{lemma:odpadlik2:A} Buď $\eqtforw[*]{(i,j)} = \eqtforw{(i,j)}$, pak tvrzení plyne přímo z předpokladu lemmatu.
		
		\item Nebo $\eqtforw[*]{(i,j)} \neq \eqtforw{(i,j)}$. Z definice algoritmu plyne (bod \ref{alg:podm1})), že platí $\eqtforw[*]{(i,j)} = \eqtforw{(i,j)} - \eqtback{(k,l)}$ (viz obrázek \ref{fig:odpadlik2-dk}). Na základě 
		\begin{itemize}
			\item podmínky algoritmu \ref{alg:podm2}) (tj. $\eqtback{(k,l)}$ je on-time, tudíž není SL), 
			\item předpokladu tohoto lemmatu ($\eqtforw{(i,j)}$ je SL) 
			\item a s pomocí lemmatu \ref{lemma:odtrzeninotSL} 
		\end{itemize}
		je zřejmé, že $\eqtforw[*]{(i,j)}$ je SL.
		
		Analogicky lze dokázat tvrzení pro backward shift.
	\end{enumerate}
\end{proof}

Z předchozích tvrzení plyne, že v již forward posunutém stromu platí pro každou jeho hranu $(i,j)$, že i po odpadnutí jednoho či více odpadlíků je $\eqtforw{(i,j)}$ SL (Analogicky pro backward shift).

Nakonec jedno pomocné lemma, které nám bude hodit při dokazování korektnosti algoritmu:

\begin{lemma}\label{lemma:ontimeSE}
	Let $(G,p,c)$ be an instance of the problem STNCONV and $\sigma$ be a schedule. Let $\widetilde{G}$ be an on-time subgraph of $G$ in $\sigma$. Let $\widetilde{U}$ is a strictly early (resp. strictly late) subgraph of $\widetilde{G}$. Then $\widetilde{G}-\widetilde{U}$ is late (resp. early).
\end{lemma}
\begin{proof}
	By contradiction: Let us assume, that $\widetilde{G}-\widetilde{U}$ isn't late. It follows, according to definition...., that $\widetilde{G}-\widetilde{U}$ is strictly early. Then, according to lemma..... $(\widetilde{G}-\widetilde{U}) \cup \widetilde{U}=\widetilde{G}$ had to be strictly early. But we know that $\widetilde{G}$ is on-time, which is a contradiction. Thus $\widetilde{G}-\widetilde{U}$ must be late.
	
	Case for strictly late $\widetilde{U}$ can be proven analogically.
\end{proof}

A další lemma které se nám bude hoditi :).

\begin{definition}
	Nechť je dán rozvrh $\sigma$. Nechť jsou dány dva equality tree $\eqt_{1}$ a $\eqt_{2}$ a hrana $(i,j)$ taková, že $i\in \act_{\eqt_{1}}$ a $j\in \act_{\eqt_{2}}$. \textbf{Merge equality tree $\eqt_{1}$ a $\eqt_{2}$ na hraně $(i,j)$} rozumíme strom 
	$\eqt=
 	  \{
 	     \act_{\eqt_{1}} \cup \act_{\eqt_{2}}, 
 	     \sa_{\eqt_{1}} \cup \sa_{\eqt_{2}} \cup \{(i,j)\}
 	  \}$.
\end{definition}

\begin{definition}
	Analogicky definovat split jako inverzní operaci k merge.
\end{definition}

\begin{lemma}\label{lemma:splitpoposunu}
	Nechť je dán rozvrh $\sigma$. Nechť jsou dány dva equality tree $\eqt_{1}$ a $\eqt_{2}$ pro které platí: $\forall (i,j)\in A_{\eqt_1}$ je $\eqtforw[1]{(i,j)}$ SL a $\forall (i,j)\in A_{\eqt_2}$ je $\eqtforw[2]{(i,j)}$ SL. Nechť je dána hrana $(k,l)$, taková že $k \in \act_{\eqt_{1}}$ a $l \in \act_{\eqt_{2}}$. Nechť equality tree $\eqt$ je merge stromů $\eqt_{1}$ a $\eqt_{2}$ na hraně $(k,l)$. Nechť $(k,l)$ je aktivní v $\eqt$ a nechť $\eqt$ je on-time, pak $\eqt$ NENÍ active equality tree, ale ty hrany, které potřebuji, jsou aktivní... nějak sem zamotat asi pivota? Tahle věta dokazuje ty hrany které algoritmus nekontroloval (všechny ostatní jsou přilepené tak, že jsou SE$\rightarrow$zbytek jinak by odpadly dříve).
\end{lemma}
\begin{proof}
	\begin{enumerate}
		\item Hrana $(k,l)$ spojující $\eqt_{1}$ a $\eqt_{2}$ je aktivní z předpokladu.
		\item\label{sec:lemma:splitpoposunu1} Je zřejmé, že (NE) všechny hrany $(i,j)\in \eqt_{2}$ platí, že jsou aktivní (jen ty které potřebuji), protože $\eqtforw{(i,j)}$ je z předpokladu SL a $\eqtback{(i,j)}$ není SL, protože celý $\eqt$ je on-time. Hrana $(i,j)$ tudíž spojuje SE nebo E strom se stromem který je SL, tudíž je aktivní.
		\item Hrany $(i,j)\in \eqt_{1}$ jsou také aktivní (NE Všechny) protože platí
		\begin{itemize}
		\item buď je $\eqt_{2}$ SL, tudíž pokud byl $\eqtforw[1]{(i,j)}$ SL, pak po merge je SL i $\eqtforw{(i,j)}$ a ze stejného důvodu jako v bodě \ref{sec:lemma:splitpoposunu1} je tudíž hrana aktivní.
		\item nebo $\eqt_{2}$ není SL. Pak protože je hrana $(k,l)$ aktivní, plyne, že $\eqt_{1}$ je SE. Z předpokladu víme, že $\eqtforw[1]{(i,j)}$ je SL. Pak ale dle lemmatu \ref{lemma:odtrzeninotSL} plyne, že $\eqtback[1]{(i,j)}$ je SE. Tudíž hrana je také aktivní.
		\end{itemize}
	\end{enumerate}
\end{proof}















Nyní provedeme samotný důkaz korektnosti algoritmu (tedy zatím jen toho, že odpadlíci jsou on-time AET):

\begin{enumerate}
	\item \label{ontime}Je odpadlík on-time? Uvažujme nyní forward shift (backward shift je analogický): Odpadlík je jistě E (kdyby nebyl early, znamenalo by to že je SL, ale to by odpadl už někdy dřív). Odpadává ve chvíli kdy není SE, tzn. že je L. Tudíž odpadlík je E i L zároveň, takže je on-time
	
	\item Je odpadlík AET? Uvažujme libovolnou hranu v odpadlíkovi (na obrázku je to $[k,l]$ - dělí odpadlíka $A$ na dvě části $A_k$ a $A_l$). Je aktivní v rámci odpadlíka? Co o ni vím?
\begin{enumerate}
	\item Uvažujme forward shift v první fázi algoritmu:
	\begin{enumerate}
		\item \label{item:odpadlikocasek} Nechť je to hrana směřující k pivotovi: Pak z podstaty algoritmu plyne, že $A_k$ je SE (jinak by odpadlo dříve). Vzhledem k lemmatu \ref{lemma:ontimeSE} a bodu \ref{ontime} pak $A_l$ musí být L. Tudíž hrana je aktivní.

		\item Nechť je to hrana směřující od pivota: 
		\begin{itemize}
			\item Pak buď byl strom již posunut forward a tudíž pro všechny jeho hrany $(i,j)$ platí, že $\eqtforw{(i,j)}$ je SL. Pak na základě stejné úvahy jako v předchozím bodě \ref{item:odpadlikocasek} je hrana aktivní.
			\item Nebo stromem ještě nebylo hnuto, pak buď je $A_k$ SL a platí stejná úvaha jako v předchozím bodě (doporučuji se podívat opět na obrázek výše). Nebo $A_k$ není SL (jistě je ale L), pak vzhledem k tomu, že hrana $(l,k)$ byla aktivní (a stromem jsme zatím nehnuli), musí být $A_l \cup B$ SE. Protože hrana $(i,j)$ byla aktivní a $A$ odpadá ve chvíli kdy není SE, pak plyne že $B$ musí být SL. Dle lemmatu \ref{lemma:odtrzeninotSL} plyne, že $A_l$ je SE a tudíž hrana $(l,k)$ je i v tomto případě aktivní. Tato úvaha není ovlivněna odpadnutím dalšího odpadlíka ve startovní pozici a lze ji tak použít postupně i na více odpadlíků ve startovní pozici.
		 \end{itemize}
	\end{enumerate}

	\item Uvažujme backward shift v druhé fázi algoritmu:\label{item:backward}
	\begin{enumerate}
		\item Nechť je to hrana směřující od pivota: Pak na základě analogické úvahy jako v \ref{item:odpadlikocasek} je hrana aktivní.		

		\item\label{item:backwardB} Nechť je to hrana směřující k pivotovi: V první fázi algoritmu byly kontrolovány všechny tyto hrany a pokud $A_k$ nebylo SE, odpadlo. Tudíž $A_k$ je SE. Vzhledem k lemmatu \ref{lemma:ontimeSE} a bodu \ref{ontime} pak $A_l$ musí být L. Tudíž hrana je aktivní.
	\end{enumerate}
\end{enumerate}
\end{enumerate}
\end{description}

Z předchozího plyne, že odpadlíci jsou on-time AET jak při forward shiftu tak i při backward shiftu. Zatím ovšem ignorujeme možné srážky s ostatními stromy v rozvrhu. 
\newpage

Do teď jsme předpokládali, že námi pushovaný strom $\eqt_{pivot}$ nenaráží do žádných jiných stromů. Tudíž při posunu $\eqt_{pivot}$ platilo lemma \ref{lemma:zachovani}, které je využíváno následně i lemmatem \ref{lemma:odpadlik2}. Tato tvrzení předpokládají, že při forward pushi ty části stromu které byly SL nemohly přestat být SL (analogicky pro backward push). Nyní ovšem do hry necháme vstoupit i další stromy, se kterými se bude $\eqt_{pivot}$ spojovat.

Nechť $\eqt$ je nějaký strom, do kterého $\eqt_{pivot}$ během forward pushe narazí a spojí se s ním přes nějakou hranu $(i,j)$. Po takové srážce už nemusí platit, že pro každou hranu $(k,l)\in A_{\eqt_{pivot}}$ je $\eqtforw{(k,l)}$ SL. Minimálně pro samotnou hranu $(i,j)$ to jistě neplatí. Musíme ukázat, že i přes to všechno jsou odpadlíci (po malé úpravě procedurou Activate()) stále on-time AET. Nakonec i ukážeme, že ve chvíli, kdy se $\eqt_{pivot}$ dostane do cíle (tj. do bodu kde je on-time na konci MakeOnTime() procedury) je $\eqt_{pivot}$ AET.

Zaměřme se nyní na určité vlastnosti pushovaného stromu po jedné srážce s jiným stromem (tj. po nějaké události merge). Oproti úvahám o odpadlících, kde jsme ignorovali srážky, budeme nyní uvažovat i odpadávání odpadlíků dle výše definovaného algoritmu. Nechť tedy provádíme operaci forward push() (backward jde dokázat analogicky) s nějakým stromem $\eqt_1$ (viz obrázek), který se cestou srazí s jedním se stromem $\eqt_2$ a operací merge jsou spojeny nějakou hranou $(i,j)$ dohromady ve strom $\eqt=\eqt_1 \cup \eqt_2$. Uvažujme nyní $\eqt_2$ izolovaně: Strom $\eqt_2$ byl on-time, tudíž po forward pushi může být dle lemmatu \ref{lemma:zachovani} nyní buď on-time nebo SL. Uvažujme nyní tyto dvě možnosti:
\begin{description}
	\item[$\eqt_2$ je on-time]: pak můžeme strom $\eqt$ na hraně $(i,j)$ opět rozdělit a víme, že $\eqt_2$ zůstane on-time AET, protože jsme v podstatě neudělali nic jiného, než že jsme posunuli on-time AET trochu více doprava. Můžeme uvažovat, jako bychom chtěli najednou začít couvat backward - to by způsobilo odpadnutí $\eqt_2$, což již dle bodu \ref{item:backward} víme, že by $\eqt_2$ byl on-time AET. 
	
	Dokonce víme, že cestou z $\eqt_2$ nic neodpadlo, protože před posunem se jednalo o on-time AET a po posunu je to také on-time AET. Jak totiž již víme, po nenulovém forward shiftu platí pro všechny hrany $(i,j)$ ve stromu, že $\eqtforw{(i,j)}$ je SL. Takže pokud by se tento strom rozpadl na libovolné hraně $(i,j)$, jeho zbytek $\eqtforw{(i,j)}$ by musel být SL.
	
	 Úvahy o $\eqt_1$ pak můžeme provádět jako by se žádný merge nestal. Tudíž lemma \ref{lemma:forwardshift} a lemma \ref{lemma:odpadlik2} platí i v tomto případě.
	 
	\item[$\eqt_2$ je SL]: pak víme, že $\eqt_2$ byl shiftnutý doprava o nenulové $\delta$ (jinak by zůstal on-time), tudíž víme, že pro každou hranu $(k,l)$ v $\eqt_2$ na základě lemmatu \ref{lemma:ontimeSE} platí, že $\eqtforw{(k,l)}$ je SL. Pak ale opět pro všechny hrany $(i,j)$ v $\eqt$ platí, že $\eqtforw{(i,j)}$ je SL.
	
	Tudíž lemma \ref{lemma:forwardshift} a lemma \ref{lemma:odpadlik2} platí i v tomto případě.
\end{description}

\begin{figure}
	\centering
	\includegraphics[scale=0.5]{bump}
\end{figure}

Pushujeme-li nějakým stromem forward, cestou nám odpadávají odpadlíci a připojujeme stromy do kterých narazíme, pak pokud se dostaneme do bodu, kdy je tento strom on time, může nastat jeho rozpad na více on-time AET, nebo sám je rovnou AET.

Zbývá zodpovědět poslední otázku: mám po dokončení druhé fáze v ruce on-time AET? Z podstaty algoritmu plyne, že mám v ruce on-time strom (tak jsem si definoval stav zastavení posouvání). Můžeme se na tento strom dívat jako na odpadlíka a použít na něj všechny výše uvedené úvahy. Pokud lze rozdělit na více on-time AET na hranách, kterými narazil do jiných stromů, tak ho rozdělit a to co mi zbude je on-time AET.

Znamená to, že algoritmus můžeme ponechat zcela nedotčený (resp. chybí nám v článku procedura acitvate() volaná pro každého odpadlíka - navíc pravděpodobně není zapotřebí kontrolovat všechny hrany, ale jen ty, kde kde proběhl merge.) a předešlým textem dokázat jeho korektnost a úplnost.

\newpage
\textbf{Zkusíme to znovu a lépe}
\begin{lemma}
Nechť odpadá odpadlík ve chvíli která není startem algoritmu a zároveň nebylo v této chvíli nic připojeno ke stromu. Pokud provedeme split na všech hranách, kterými byly připojeny nějaké nárazové stromy, a které nejsou aktivní, pak vzniklý les z odpadlíka je on-time active equality forest.
\end{lemma}
\begin{proof}
Označme odpadlíka jako $\eqt$. Celým $\eqt$ bylo posunuto forward (stromy k němu dříve připojené operací merge byly také posunuty). Tudíž v rámci každého z připojených stromů a v rámci původní části stromu platí, že $\forall \eqtforw[*]{(i,j)}$ je SL. Vím že pokud jsem něco splitnul - rozpadlo se to na dva on-time stromy, protože levá strana této hrany byla jistě early a pravá late - rozpadlo se to proto, že ani jedna strana nebyla 'strictly'. 
\end{proof}

\end{document}